• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文OA文献 >An experimental Study using ACSL and Frama-C to formulate and verify Low-Level Requirements from a DO-178C compliant Avionics Project
【2h】

An experimental Study using ACSL and Frama-C to formulate and verify Low-Level Requirements from a DO-178C compliant Avionics Project

机译：使用aCsL和Frama-C进行配制和验证的实验研究   符合DO-178C标准的航空电子设备项目的低级要求

代理获取
本网站仅为用户提供外文OA文献查询和代理获取服务，本网站没有原文。下单后我们将采用程序或人工为您竭诚获取高质量的原文，但由于OA文献来源多样且变更频繁，仍可能出现获取不到、文献不完整或与标题不符等情况，如果获取不到我们将提供退款服务。请知悉。
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Safety critical avionics software is a natural application area for formalverification. This is reflected in the formal method's inclusion into thecertification guideline DO-178C and its formal methods supplement DO-333.Airbus and Dassault-Aviation, for example, have conducted studies in usingformal verification. A large German national research project, Verisoft XT,also examined the application of formal methods in the avionics domain. However, formal methods are not yet mainstream, and it is questionable ifformal verification, especially formal deduction, can be integrated into thesoftware development processes of a resource constrained small or mediumenterprise (SME). ESG, a Munich based medium sized company, has conducted asmall experimental study on the application of formal verification on a smallportion of a real avionics project. The low level specification of a softwarefunction was formalized with ACSL, and the corresponding source code waspartially verified using Frama-C and the WP plugin, with Alt-Ergo as automatedprover. We established a couple of criteria which a method should meet to be fit forpurpose for industrial use in SME, and evaluated these criteria with theexperience gathered by using ACSL with Frama-C on a real world example. Thepaper reports on the results of this study but also highlights some issuesregarding the method in general which, in our view, will typically arise whenusing the method in the domain of embedded real-time programming.
机译：安全关键的航空电子软件是形式验证的自然应用领域。这体现在正式方法被纳入认证指南DO-178C中，其正式方法是对DO-333的补充。例如，空中客车公司和Dassault-Aviation已在使用正式验证方面进行了研究。德国的一个大型国家研究项目Verisoft XT也研究了形式方法在航空电子领域的应用。但是，形式化方法尚未成为主流，并且能否将形式化验证（尤其是形式化演绎）集成到资源受限的中小型企业（SME）的软件开发过程中，这是一个问题。 ESG是一家慕尼黑的中型公司，已针对正式航空电子项目中的一小部分进行了形式验证的应用实验。软件功能的低级规范已使用ACSL进行了规范化，相应的源代码已使用Frama-C和WP插件（以Alt-Ergo作为自动验证器）进行了部分验证。我们建立了一些标准，该标准应适用于中小型企业的工业用途，并以ACSL与Frama-C结合使用为例，对这些标准进行了评估。该论文报告了这项研究的结果，但同时也强调了与该方法有关的一些问题，我们认为，在嵌入式实时编程领域中使用该方法时，通常会出现这些问题。

著录项

  • 作者

    Dordowsky, Frank;

  • 作者单位
  • 年度 2015
  • 总页数
  • 原文格式 PDF
  • 正文语种
  • 中图分类

相似文献

  • 外文文献
  • 中文文献
  • 专利
代理获取

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号